es:ES, Qa, Rb:(EE), A, B:Type, Ia:AbsInterface(A), Ib:AbsInterface(B), f, g:Top.
es-interface-empty(es;Ia)  es-interface-empty(es;Ib)  g glues Ia:Qa f Ib:Rb 

latex

Definitions

x:A. B(x), {x:A| B(x)} , Void, s = t, E, b, x:AB(x), f(a), t  T, , P  Q, x:A  B(x), P & Q, x:A. B(x), case b of inl(x) => s(x) | inr(y) => t(y), True, e  X, if b then t else f fi , Type, left + right, (e < e'), P  Q, e c e', A, Top, AbsInterface(A), ES, E(X), Inj(A;B;f), f is Q-R-pre-preserving on P, es-interface-empty(es;I), Q ==f== P, {I}, Q = f== P, g glues Ia:Qa f Ib:Rb, False